the_w:World, e:E, t:.
FairFifo
 isrcv(kind(e))
 match(lnk(kind(e));t;time(e))
 onlnk(lnk(kind(e));m(source(lnk(kind(e)));t))
 [||rcvs(lnk(kind(e));time(e))||-||snds(lnk(kind(e));t)||]
 =
 msg(a(loc(e);time(e)))
  Msg 

latex

Definitions	t  T, #$n, x:A. B(x), AB, P & Q, i  j < k, {x:A| B(x) }, , {i..j}, x:AB(x), P  Q, <a,b>, time(e), False, A, {T}, SQType(T), Prop, s ~ t, x:AB(x), x:A. B(x), World, E, FairFifo, kind(e), isrcv(k), b, lnk(k), match(l;t;t'), m(i;t), onlnk(l;mss), l[i], Msg, , s = t
Lemmas	w-match wf, lnk wf, w-time wf, assert wf, isrcv wf, w-ekind wf, fair-fifo wf, nat wf, w-E wf, world wf, better-w-match-exists, w-match-unique, le wf